% eager.chr====================================================================
% constraint handling rules for linear arithmetic
% thom fruehwirth 910610,911213,920124,930518,931223
% complete for equations, makes most equalities ecplicit, slower than 'lazy'
% may loop if variables of the equations are unified

handler eager.

option(already_in_store, off). 
option(already_in_heads, off).
option(check_guard_bindings, off).

% load handler for inequalities (that introduces slack variables)
:- ['math-ineq.pl'].

operator(100,xfx,equals).
constraints (equals)/2. 

% simplify single equation
empty @ [] equals C1 <=> zero(C1).
unify @ [X*C2] equals C1 <=> nonground(X) | is_div(C1,C2,X). % nonzero(X)
simplify @ P0 equals C1 <=> delete(X*C2,P0,P), ground(X) |
	is_mul(X,C2,XC2),
	C is XC2+C1, 
	P equals C.

/*
% lazy rule to replace a variable
eliminate @ [X*C2X|PX] equals C1X \ [X*C2|P] equals C1 <=> %var(X) | 
	is_div(C2,C2X,CX), 
	mult_const(eq0(C1X,PX),CX,P2),	
        add_eq0(eq0(C1,P),P2,eq0(C3,P3)),
	sort1(P3,P4),
	P4 equals C3.
*/
% eager rule to replace a variable or slack
eliminate @ [X*C2X|PX] equals C1X \ P0 equals C1 <=> delete(Y*C2,P0,P),X==Y | 
	is_div(C2,C2X,CX), 
	mult_const(eq0(C1X,PX),CX,P2),	
        add_eq0(eq0(C1,P),P2,eq0(C3,P3)),
	P3 equals C3.


% handle slack variables
slack @ P equals C <=> all_slacks(P,PS),sign(C,CS),(CS=0;CS=PS) | 
	CS=0,all_zeroes(P).


% handle nonlinear equations
operator(450,xfx,eqnonlin).
constraints (eqnonlin)/2.
linearize @ X eqnonlin A   <=> ground(A) | A1 is A, X=:=A1.
linearize @ X eqnonlin A*B <=> ground(A) | A1 is A, X=:=A1*B.
linearize @ X eqnonlin B*A <=> ground(A) | A1 is A, X=:=A1*B.


/* end of file eager.chr ---------------------------------------------------*/